| 1: | active(f(a,b,X)) | → mark(f(X,X,X)) | |
| 2: | active(c) | → mark(a) | |
| 3: | active(c) | → mark(b) | |
| 4: | active(f(X1,X2,X3)) | → f(active(X1),X2,X3) | |
| 5: | active(f(X1,X2,X3)) | → f(X1,X2,active(X3)) | |
| 6: | f(mark(X1),X2,X3) | → mark(f(X1,X2,X3)) | |
| 7: | f(X1,X2,mark(X3)) | → mark(f(X1,X2,X3)) | |
| 8: | proper(f(X1,X2,X3)) | → f(proper(X1),proper(X2),proper(X3)) | |
| 9: | proper(a) | → ok(a) | |
| 10: | proper(b) | → ok(b) | |
| 11: | proper(c) | → ok(c) | |
| 12: | f(ok(X1),ok(X2),ok(X3)) | → ok(f(X1,X2,X3)) | |
| 13: | top(mark(X)) | → top(proper(X)) | |
| 14: | top(ok(X)) | → top(active(X)) | |
| 15: | ACTIVE(f(a,b,X)) | → F(X,X,X) | |
| 16: | ACTIVE(f(X1,X2,X3)) | → F(active(X1),X2,X3) | |
| 17: | ACTIVE(f(X1,X2,X3)) | → ACTIVE(X1) | |
| 18: | ACTIVE(f(X1,X2,X3)) | → F(X1,X2,active(X3)) | |
| 19: | ACTIVE(f(X1,X2,X3)) | → ACTIVE(X3) | |
| 20: | F(mark(X1),X2,X3) | → F(X1,X2,X3) | |
| 21: | F(X1,X2,mark(X3)) | → F(X1,X2,X3) | |
| 22: | PROPER(f(X1,X2,X3)) | → F(proper(X1),proper(X2),proper(X3)) | |
| 23: | PROPER(f(X1,X2,X3)) | → PROPER(X1) | |
| 24: | PROPER(f(X1,X2,X3)) | → PROPER(X2) | |
| 25: | PROPER(f(X1,X2,X3)) | → PROPER(X3) | |
| 26: | F(ok(X1),ok(X2),ok(X3)) | → F(X1,X2,X3) | |
| 27: | TOP(mark(X)) | → TOP(proper(X)) | |
| 28: | TOP(mark(X)) | → PROPER(X) | |
| 29: | TOP(ok(X)) | → TOP(active(X)) | |
| 30: | TOP(ok(X)) | → ACTIVE(X) | |